Adding new PyK wrappers to LLVM Python Bindings #4426
Conversation
Robertorosmaninho
requested review from
theo25,
gtrepta,
dwightguth,
Baltoli and
tothtamas28
There was a problem hiding this comment.
A couple of minor comments, and I'll let @tothtamas28 provide a final review as well in case I've missed anything.
|
This is the new rendered comments: |
| input_kore_file = kompile._cache_definition(self.HINTS_INPUT_KORE) | ||
| hints_file_name = definition_dir.name.replace('.k', '.hints') |
There was a problem hiding this comment.
This looks a bit hacky. Consider implementing a dedicated cache of hints inputs for ProofTraceTest. Then no renaming is needed, and kompiler can be dropped as a direct dependency.
(After the renaming, the cache might no longer point to the right file.)
There was a problem hiding this comment.
The renaming is just for creating a new file with a custom name instead of simply ‘hints.bin’ or something static like this. This is mainly to avoid the use of 2 different tests appending in the same file (an issue that I found while writing those tests).
|
Ping @Baltoli |
This PR exposes the new infrastructure created by the LLVm Backend to parse the Hints file.
We introduce the wrappers to make the streaming parser possible to use as a list of events and access it through an integrator. Or not loading all the events at the same time but accessing them one per time through the
next()function.Depends on: runtimeverification/llvm-backend#1090